package alloy.symm;


import java.util.Set;
import java.util.TreeSet;

import alloy.ast.Expr;
import alloy.ast.LeafExpr;
import alloy.ast.LeafId;
import alloy.ast.QuantifiedExpr;
import alloy.ast.Quantifier;

/**
 * Finds unary relations that are constrained to be lone sets (i.e. contain at most one tuple).
 * <p>
 * We look for unary relations r for which the fact "lone r" is conjoined at the top of the translatable AST formula.
 */
class LoneSetDetector_V extends TopLevelConjVisitor {
    /**
     * Lone sets we have found: {@link LeafId}s of unary relations that --
     * we have determined -- are constrained to be lones in any solution.
     */
    private Set /* of LeafId */ _loneSetIds = new TreeSet();
    
    //--------//
    // Methods//
    //--------//
    
    LoneSetDetector_V() { }

    /** Test whether the given relation is unary and is constrained to contain at most one tuple. */
    boolean isLoneSet(LeafId leafId_) {
        return _loneSetIds.contains(leafId_);
    }

    /** Return the Set of {@link LeafId}s of lone unary relations that we have found. */
    Set /* of LeafId */ getLoneSetIds() { return _loneSetIds; }
    
    /**
     * For a top-level conjunct of the form "lone r" where <code>r</code> is a relation,
     * record the {@link LeafId} of <code>r</code>.
     */
    public void visit(QuantifiedExpr quantExpr_) {
		Quantifier quant = quantExpr_.getQuantifier();
		if (quant.equals(Quantifier.ONE) || quant.equals(Quantifier.LONE)) {
		    Expr expr = quantExpr_.getExpr();
		    if (_isRelation(expr) && _isUnary(expr)) {
			_loneSetIds.add(((LeafExpr)expr).getLeafId());
		    }
		}
    }
    
}
